Nuprl Lemma : R-occurs_wf 11,40

R:es_realizer{i:l}, z,i:Id. R-occurs(Riz  
latex


Definitionsx,y,z,w,vt(x;y;z;w;v), x,y,z,u,v,wt(x;y;z;u;v;w), x,y,zt(x;y;z), x,y,z,wt(x;y;z;w), xt(x), R-occurs(Riz), t  T, x:AB(x), x(s1,s2,s3,s4,s5), x(a,b,c,d,e,f), x(s1,s2,s3), x(s1,s2,s3,s4), x(s), Unit, es_realizer{i:l}, Rrframe(locxL), Rbframe(lockL), Raframe(lockL), Rpre(locdsapP), Rsends(dskndTldtg), Reffect(locdskndTxf), Rsframe(lnktagL), Rframe(locTxL), Rinit(locTxv), Rplus(leftright), Rnone,
Lemmasdeq-member wf, lsrc wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, eq id wf, band wf, es realizer wf, es realizer ind wf, bor wf, bfalse wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf

origin